COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00009 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.cb EXPANDING THE ROLE OF VERIFICATION IN COMPUTER SCIENCE EDUCATION


	The fact that computer programs are still debugged
is a continuing disgrace to anyone who thinks mathematically.
The way of getting a program correct should be to prove that it
meets its specifications and check this proof with a computer.
As much as possible, the proof should be computer generated.

	Of course, this has been the goal of program verification
research for many years, and good progress has been made.
Even though verification has not progressed to a point permitting
large practical programs to be verified instead of debugged, it
has reached the point where students in programming courses will
benefit from verifying many of the programs they write.

	 The benefits are twofold:
First, a student who has verified a program understands what it
does far better than one who has merely tinkered with it till it
works.  Second, if he must verify his programs, the student will find
the exercise easier if he makes a well structured prgram even at the
cost of rewriting it as his understanding improves.  For example, none
of the bad SAMEFRINGE programs published in the SIGART Newsletter
last year would have survived an attempt by the authors to verify
them.

	Introducing verification into the teaching of programming
will require much work.  Here is a plan for achieving it at
Stanford:
.item←0

	#. Verification should be separated from complexity theory,
automata theory and formal language theory as a qualifying exam
area and as a section of the comprehensive exam.  Verification
should include Hoare-type methods, verification condition generation,
the Cartwright-McCarthy method of expressing LISP programs by
first order sentences and schemata, and the Scott formalisms.  A first step is
the preparation of a qualifying exam syllabus.

	#. A subset of this should be on the comprehensive syllabus.
This should include and might be limited to the material on invariants
in Manna's book and the material on first order representation in
the McCarthy and Talcott book.  The necessary background in first
order logic might be included in this part of the syllabus, especially
since it is in the Manna book.

	#. The programming problem on the Comprehensive should require
that the program be verified.  Given the present state of verification,
this would probably require making it somewhat less ambitious as
a programming problem, but this part of the exam has already received
much criticism as not a scientific exercise.  This cannot be done
until the one or another of the machine verification systems has
been made available for general use.

	#. The LISP course, now 206, and soon to be 126, should require
machine verification of some of its programs, perhaps all pure LISP
programs.  This requires the implementation of a predicate calculus
proof-checker as a feature of the student Maclisp system.  Making such
a system will be a major task, and we should get NSF to support a
project aimed at this goal.

	#. CS105 and 106 should contain some verification.  The goal
of a machine-aided verification system for these courses is vaguer
in my mind, and therefore to me seems further off.  However, perhaps
the PASCAL enthusiasts would think otherwise and would be prepared to
undertake to produce a PASCAL verification system that could be used
in elementary courses.
Most likely such a project would also require outside support.

	#. It is possible that large amounts of student verification
will increase our computer power requirements.

	Stanford has strong enough faculty interests in verification
including Floyd (not presently active here), Luckham, Manna, McCarthy,
and Owicki, so that we are in a good position to initiate the effort.
Weyhrauch, Talcott and Karp strengthen this effort.

	A large project supported by the education part of NSF aimed
at making it practical to include verification in programming courses
might be a good form of organization.